InforLorV4, Main, Exploration, bibRecord, 003180

Compiling and securing cryptographic protocols

Identifieur interne : 003180 ( Main/Exploration ); précédent : 003179; suivant : 003181

Compiling and securing cryptographic protocols

Auteurs : Yannick Chevalier [France] ; Michaël Rusinowitch [France]

Source :

Information processing letters [ 0020-0190 ] ; 2010.

RBID : Pascal:10-0064392

Descripteurs français

Pascal (Inist)
- Translation, Compilation, Analyse décision, Réutilisation, Primitif, Méthode formelle, Système sécurité, Système numérique, Informatique théorique, Traitement information, Analyse algorithme, Problème décision, Protocole cryptographique.

English descriptors

KwdEn :
- Algorithm analysis, Compilation, Computer theory, Cryptographic protocol, Decision analysis, Digital system, Formal method, Information processing, Primitive, Reuse, Safety systems, Translation.
mix :
- Cryptographic protocols, Dolev Yao model, Formal methods, Protocol compiling, Roles, Safety/security in digital systems.

Abstract

Protocol narrations are widely used in security as semi-formal notations to specify conversations between roles. We define a translation from a protocol narration to the sequences of operations to be performed by each role. Unlike previous works, we reduce this compilation process to well-known decision problems in formal protocol analysis. This allows one to define a natural notion of prudent translation and to reuse many known results from the literature in order to cover more crypto-primitives. In particular this work is the first one to show how to compile protocols parameterised by the properties of the available operations.

Url:

https://hal.inria.fr/inria-00527633

Affiliations:

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Compiling and securing cryptographic protocols</title>
<author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>Loria, Inria Nancy Grand Est, Campus Scientifique - BP</s1>
<s2>239 54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>Loria, Inria Nancy Grand Est, Campus Scientifique - BP</s1>
<s2>239 54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">10-0064392</idno>
<date when="2010">2010</date>
<idno type="stanalyst">PASCAL 10-0064392 INIST</idno>
<idno type="RBID">Pascal:10-0064392</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000243</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000775</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000179</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000179</idno>
<idno type="wicri:doubleKey">0020-0190:2010:Chevalier Y:compiling:and:securing</idno>
<idno type="wicri:Area/Main/Merge">003242</idno>
<idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00527633</idno>
<idno type="url">https://hal.inria.fr/inria-00527633</idno>
<idno type="wicri:Area/Hal/Corpus">001680</idno>
<idno type="wicri:Area/Hal/Curation">001680</idno>
<idno type="wicri:Area/Hal/Checkpoint">002861</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">002861</idno>
<idno type="wicri:doubleKey">0020-0190:2010:Chevalier Y:compiling:and:securing</idno>
<idno type="wicri:Area/Main/Merge">003332</idno>
<idno type="wicri:Area/Main/Curation">003180</idno>
<idno type="wicri:Area/Main/Exploration">003180</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Compiling and securing cryptographic protocols</title>
<author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>Loria, Inria Nancy Grand Est, Campus Scientifique - BP</s1>
<s2>239 54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>Loria, Inria Nancy Grand Est, Campus Scientifique - BP</s1>
<s2>239 54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Information processing letters</title>
<title level="j" type="abbreviated">Inf. process. lett.</title>
<idno type="ISSN">0020-0190</idno>
<imprint><date when="2010">2010</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Information processing letters</title>
<title level="j" type="abbreviated">Inf. process. lett.</title>
<idno type="ISSN">0020-0190</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Algorithm analysis</term>
<term>Compilation</term>
<term>Computer theory</term>
<term>Cryptographic protocol</term>
<term>Decision analysis</term>
<term>Digital system</term>
<term>Formal method</term>
<term>Information processing</term>
<term>Primitive</term>
<term>Reuse</term>
<term>Safety systems</term>
<term>Translation</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Translation</term>
<term>Compilation</term>
<term>Analyse décision</term>
<term>Réutilisation</term>
<term>Primitif</term>
<term>Méthode formelle</term>
<term>Système sécurité</term>
<term>Système numérique</term>
<term>Informatique théorique</term>
<term>Traitement information</term>
<term>Analyse algorithme</term>
<term>Problème décision</term>
<term>Protocole cryptographique</term>
</keywords>
<keywords scheme="mix" xml:lang="en"><term>Cryptographic protocols</term>
<term>Dolev Yao model</term>
<term>Formal methods</term>
<term>Protocol compiling</term>
<term>Roles</term>
<term>Safety/security in digital systems</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Protocol narrations are widely used in security as semi-formal notations to specify conversations between roles. We define a translation from a protocol narration to the sequences of operations to be performed by each role. Unlike previous works, we reduce this compilation process to well-known decision problems in formal protocol analysis. This allows one to define a natural notion of prudent translation and to reuse many known results from the literature in order to cover more crypto-primitives. In particular this work is the first one to show how to compile protocols parameterised by the properties of the available operations.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Vandœuvre-lès-Nancy</li>
</settlement>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name>
</region>
<name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003180 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003180 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Pascal:10-0064392
   |texte=   Compiling and securing cryptographic protocols
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

Serveur d'exploration sur la recherche en informatique en Lorraine

Compiling and securing cryptographic protocols

Compiling and securing cryptographic protocols

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.